i:Id, ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, v:T, ks:Knd List,
tr:(k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)TT).
ds || x : T
 Normal(T)
 (k:Knd. (k  ks)  isrcv(k)  i = destination(lnk(k)))
 Normal(ds)
 Normal(da)
 R-state-var-init(i;ds;da;x;T;v;ks;tr)
 ||- es.es-decls(es;i;ds;da)
 ||- es. vartype(i;x)  T
 ||- es. & e@i.
 ||- es. & (x after e) = es-trans-state-from{i:l}(es;ks;tr;v;es-init(es;e);e)  T
 ||- es. & & (first(e)  (x when e) = v  T) 

latex

Definitions

x:A. B(x), P  Q, t  T, Prop, x. t(x), A & B, e@i. P(e), e'e.P(e'), e  e' , P  Q, R-state-var(i;ds;da;x;T;ks;tr), State(ds), DeclaredType(ds;x), Top, P  Q, P  Q, P & Q, Id, A || B, Y, if b t else f fi, Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), True, R-loc(R), Rds(R), Rda(R), p = q, R-base-domain(R), R-frame-compat(A;B), R-interface-compat(A;B), p  q, i=j, 1of(t), 2of(t), true, Reffect?(x1), Rframe?(x1), Rframe-x(x1), Reffect-x(x1), Reffect-knd(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Rrframe?(x1), Rrframe-x(x1), Reffect-ds(x1), Rrframe-L(x1), Rsends?(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsends-l(x1), Rsframe-tag(x1), Rsends-g(x1), Rsends-knd(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rpre-ds(x1), Rpre-a(x1), Rsends-dt(x1), Reffect-T(x1), Rsends-T(x1), false, SQType(T), {T}, R-state-var-init(i;ds;da;x;T;v;ks;tr), b, Normal(T), x(s), Valtype(da;k), , Unit, @i x initially v:T,

Lemmas

R-state-var-rule, R-init-rule, R-and-rule, R-state-var wf, Rinit wf, init-p wf, normal-da wf, normal-ds wf, Knd wf, l member wf, assert wf, isrcv wf, Id wf, ldst wf, lnk wf, normal-type wf, fpf-compatible wf, id-deq wf, fpf-single wf, decl-state wf, ma-valtype wf, fpf wf, es-locl wf, es-after wf, es-le-loc, es-vartype wf, R-compat-symmetry, R-compat-Rplus2, Rall wf, Reffect wf, fpf-join wf, Rframe wf, subtype rel dep function, fpf-cap wf, top wf, subtype rel self, fpf-cap-join-subtype, fpf-compatible-join-cap, fpf-cap-single1, R-compat-Rall, eq id wf, bool wf, iff transitivity, eqtt to assert, assert-eq-id, Id sq, fpf-compatible-join, fpf-compatible-symmetry, deq wf, fpf-compatible-self, fpf-empty-compatible-left, Kind-deq wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, fpf-empty-compatible-right, fpf-empty wf, R-implies-rule, Rplus wf, alle-at wf, es-loc wf, es-when wf, es-first wf, es-E wf, es-init wf, es-loc-init, es-init-le, es-when-first, es-first-init